
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.ErgoC.Lang.ErgoCType</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.ErgoC.Lang.ErgoCType" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.ErgoC.Lang.ErgoCType</h1>
<div class="coq">
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html">List</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Program.Basics.html">Basics</a></span>.<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html">ErgoSpec.Backend.ErgoBackend</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Misc.html">ErgoSpec.Common.Utils.Misc</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html">ErgoSpec.Common.Utils.Names</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html">ErgoSpec.Common.Utils.NamespaceContext</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html">ErgoSpec.Common.Utils.Result</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html">ErgoSpec.Common.Utils.Provenance</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html">ErgoSpec.Common.Utils.Ast</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html">ErgoSpec.Common.Utils.PrintTypedData</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html">ErgoSpec.Common.Types.ErgoTypetoErgoCType</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html">ErgoSpec.ErgoC.Lang.ErgoC</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html">ErgoSpec.ErgoC.Lang.ErgoCTypeContext</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html">ErgoSpec.Ergo.Lang.Ergo</a></span>.<br/>
<br/>
<span class="kwd">Section</span> <span class="id"><a name="ErgoCType">ErgoCType</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Context</span> {<span class="id">m</span> : <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.TypeSystem.TBrandModel.html#brand_model">brand_model</a></span>}.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Import</span> <span class="id">ErgoCTypes</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergoc_type_join_safe">ergoc_type_join_safe</a></span> <span class="id">prov</span> (<span class="id">t1</span> <span class="id">t2</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">jt</span> := <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_join">ergoc_type_join</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#t1">t1</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#t2">t2</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_subtype_dec">ergoc_type_subtype_dec</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ttop">ttop</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#jt">jt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#prov">prov</a></span> ("<span class="id">Join</span> <span class="id">between</span> <span class="id">types</span> <span class="id">is</span> <span class="id">TOP</span>.")%<span class="id">string</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#jt">jt</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergoc_type_meet_safe">ergoc_type_meet_safe</a></span> <span class="id">prov</span> (<span class="id">t1</span> <span class="id">t2</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">jt</span> := <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_meet">ergoc_type_meet</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#t1">t1</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#t2">t2</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_subtype_dec">ergoc_type_subtype_dec</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#jt">jt</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbottom">tbottom</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#prov">prov</a></span> ("<span class="id">Meet</span> <span class="id">between</span> <span class="id">types</span> <span class="id">is</span> <span class="id">BOTTOM</span>.")%<span class="id">string</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#jt">jt</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Program</span> <span class="kwd">Definition</span> <span class="id"><a name="empty_rec_type">empty_rec_type</a></span> : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> := <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.TypeSystem.RType.html#Rec">Rec</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.TypeSystem.RType.html#Closed">Closed</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="id">_</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_format_unop_error">ergo_format_unop_error</a></span> <span class="id">nsctxt</span> (<span class="id">op</span> : <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#unary_op">unary_op</a></span>) (<span class="id">arg</span> : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">fmt_easy</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">fun</span> <span class="id">name</span> <span class="id">expected</span> <span class="id">actual</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;("<span class="id">Operator</span> `" ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> ++ "' <span class="id">expected</span> <span class="id">an</span> <span class="id">operand</span> <span class="id">of</span> <span class="id">type</span> `" ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected">expected</a></span>) ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"' <span class="id">but</span> <span class="id">received</span> <span class="id">an</span> <span class="id">operand</span> <span class="id">of</span> <span class="id">type</span> `" ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual">actual</a></span>) ++ "'.")%<span class="id">string</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#op">op</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpNeg">OpNeg</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "!"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbool">tbool</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#arg">arg</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpFloatUnary">OpFloatUnary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#FloatNeg">FloatNeg</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "-"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#arg">arg</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpDot">OpDot</a></span> <span class="id">name</span> =&gt; "<span class="id">The</span> <span class="id">field</span> " ++ <span class="id">name</span> ++ " <span class="id">does</span> <span class="id">not</span> <span class="id">belong</span> <span class="id">to</span> <span class="id">type</span> `" ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#arg">arg</a></span>) ++ "'"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">_</span> =&gt; "<span class="id">This</span> <span class="id">operator</span> <span class="id">received</span> <span class="id">an</span> <span class="id">unexpected</span> <span class="id">argument</span> <span class="id">of</span> <span class="id">type</span> `" ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#arg">arg</a></span>) ++ "'"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_format_binop_error">ergo_format_binop_error</a></span> <span class="id">nsctxt</span> (<span class="id">op</span> : <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#binary_op">binary_op</a></span>) (<span class="id">arg1</span> : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) (<span class="id">arg2</span> : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">fmt_easy</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">fun</span> <span class="id">name</span> <span class="id">e1</span> <span class="id">e2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;("<span class="id">Operator</span> `" ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> ++ "' <span class="id">expected</span> <span class="id">operands</span> <span class="id">of</span> <span class="id">type</span> `" ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#e1">e1</a></span>) ++ "' <span class="id">and</span> `" ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#e2">e2</a></span>) ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"' <span class="id">but</span> <span class="id">received</span> <span class="id">operands</span> <span class="id">of</span> <span class="id">type</span> `" ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#arg1">arg1</a></span>) ++ "' <span class="id">and</span> `" ++<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#arg2">arg2</a></span>) ++ "'.")%<span class="id">string</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#op">op</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpAnd">OpAnd</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "<span class="id">and</span>"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbool">tbool</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbool">tbool</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpOr">OpOr</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "<span class="id">or</span>"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbool">tbool</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbool">tbool</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatBinary">OpFloatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatPlus">FloatPlus</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "+"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatBinary">OpFloatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatMinus">FloatMinus</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "-"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatBinary">OpFloatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatMult">FloatMult</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "*"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatBinary">OpFloatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatDiv">FloatDiv</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "/"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatBinary">OpFloatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatPow">FloatPow</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "^"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpNatBinary">OpNatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#NatPlus">NatPlus</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "+<span class="id">i</span>"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tnat">tnat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tnat">tnat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpNatBinary">OpNatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#NatMinus">NatMinus</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "-<span class="id">i</span>"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tnat">tnat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tnat">tnat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpNatBinary">OpNatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#NatMult">NatMult</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "*<span class="id">i</span>"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tnat">tnat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tnat">tnat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpNatBinary">OpNatBinary</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#NatDiv">NatDiv</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "/<span class="id">i</span>"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tnat">tnat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tnat">tnat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpNatBinary">OpNatBinary</a></span> <span class="id">NatPow</span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "^<span class="id">i</span>"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tnat">tnat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tnat">tnat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatCompare">OpFloatCompare</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatLt">FloatLt</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "&lt;"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatCompare">OpFloatCompare</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatLe">FloatLe</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "&lt;="%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatCompare">OpFloatCompare</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatGt">FloatGt</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "&gt;"%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpFloatCompare">OpFloatCompare</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#FloatGe">FloatGe</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_easy">fmt_easy</a></span> "&gt;="%<span class="id">string</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">_</span> =&gt; "<span class="id">This</span> <span class="id">operator</span> <span class="id">received</span> <span class="id">unexpected</span> <span class="id">arguments</span> <span class="id">of</span> <span class="id">type</span> `" ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#arg1">arg1</a></span>) ++ "' " ++ " <span class="id">and</span> `" ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#arg2">arg2</a></span>) ++ "'."<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_format_new_error">ergo_format_new_error</a></span> <span class="id">nsctxt</span> (<span class="id">name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) (<span class="id">actual</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">concept_name</span> := <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> (<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.TypeSystem.RType.html#Brand">Brand</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.diff_record_types">diff_record_types</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>) <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual">actual</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; "<span class="id">Concept</span> <span class="id">name</span> " ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> ++ " <span class="id">does</span> <span class="id">not</span> <span class="kwd">match</span> <span class="id">data</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.fields_that_are_not_subtype">fields_that_are_not_subtype</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>) <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual">actual</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> =&gt; "<span class="id">Concept</span> " ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> ++ " <span class="id">doesn</span>'<span class="id">t</span> <span class="kwd">match</span> <span class="id">data</span> (<span class="id">one</span> <span class="id">field</span> <span class="id">is</span> <span class="id">not</span> <span class="id">a</span> <span class="id">subtype</span>)"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id">expected_name</span>, <span class="id">expected_type</span>, <span class="id">actual_type</span>) :: <span class="id">_</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">Field</span> `" ++ <span class="id">expected_name</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "' <span class="id">has</span> <span class="id">type</span> `" ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id">actual_type</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "' <span class="id">but</span> <span class="id">should</span> <span class="id">have</span> <span class="id">type</span> `" ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id">expected_type</span>) ++ "'"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id">actual_name</span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">Unknown</span> <span class="id">field</span> `" ++ <span class="id">actual_name</span> ++ "' <span class="kwd">in</span> <span class="id">type</span> `" ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#concept_name">concept_name</a></span> ++ "'"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id">actual_names</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">Unknown</span> <span class="id">fields</span> `" ++ <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#concat">String.concat</a></span> "', `" <span class="id">actual_names</span> ++ "' <span class="kwd">in</span> <span class="id">type</span> `" ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#concept_name">concept_name</a></span> ++ "'"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id">expected_name</span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id">_</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">Missing</span> <span class="id">field</span> `" ++ <span class="id">expected_name</span> ++ "' <span class="kwd">in</span> <span class="id">type</span> `" ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#concept_name">concept_name</a></span> ++ "'"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id">expected_names</span>, <span class="id">_</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">Missing</span> <span class="id">fields</span> `" ++ <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#concat">String.concat</a></span> "', `" <span class="id">expected_names</span> ++ "' <span class="kwd">in</span> <span class="id">type</span> `" ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#concept_name">concept_name</a></span> ++ "'"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_format_clause_return_fallback_error">ergo_format_clause_return_fallback_error</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">nsctxt</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">actual</span> <span class="id">expected</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">actual_s</span> := <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual">actual</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">expected_s</span> := <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected">expected</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">Clause</span> " ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> ++ " <span class="id">should</span> <span class="kwd">return</span> `" ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected_s">expected_s</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "' <span class="id">but</span> <span class="id">actually</span> <span class="id">returns</span> `" ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual_s">actual_s</a></span> ++ "'".<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_format_clause_return_component_error">ergo_format_clause_return_component_error</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">nsctxt</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">component1</span> <span class="id">component2</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">actual</span> <span class="id">expected</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">actual_s</span> := <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual">actual</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">expected_s</span> := <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected">expected</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">Clause</span> " ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> ++ " <span class="id">should</span> " ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#component1">component1</a></span> ++ " `" ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected_s">expected_s</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "' <span class="id">but</span> <span class="id">actually</span> " ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#component2">component2</a></span> ++ " `" ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual_s">actual_s</a></span> ++ "'".<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_format_clause_return_normal_error">ergo_format_clause_return_normal_error</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">nsctxt</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">actual</span> <span class="id">expected</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">actual_quad</span> <span class="id">expected_quad</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> * <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> * <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> * <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">actual_resp</span>, <span class="id">actual_emit</span>, <span class="id">actual_state</span>, <span class="id">actual_error</span>) := <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual_quad">actual_quad</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> '(<span class="id">expected_resp</span>, <span class="id">expected_emit</span>, <span class="id">expected_state</span>, <span class="id">expected_error</span>) := <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected_quad">expected_quad</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_subtype_dec">ergoc_type_subtype_dec</a></span> <span class="id">actual_resp</span> <span class="id">expected_resp</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_subtype_dec">ergoc_type_subtype_dec</a></span> <span class="id">actual_emit</span> <span class="id">expected_emit</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_subtype_dec">ergoc_type_subtype_dec</a></span> <span class="id">actual_state</span> <span class="id">expected_state</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_subtype_dec">ergoc_type_subtype_dec</a></span> <span class="id">actual_error</span> <span class="id">expected_error</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_clause_return_fallback_error">ergo_format_clause_return_fallback_error</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual">actual</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected">expected</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_clause_return_component_error">ergo_format_clause_return_component_error</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> "<span class="tactic">fail</span> <span class="kwd">with</span>" "<span class="id">fails</span> <span class="kwd">with</span>" <span class="id">actual_error</span> <span class="id">expected_error</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_clause_return_component_error">ergo_format_clause_return_component_error</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> "<span class="tactic">set</span> <span class="id">state</span>" "<span class="id">sets</span> <span class="id">state</span>" <span class="id">actual_state</span> <span class="id">expected_state</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_clause_return_component_error">ergo_format_clause_return_component_error</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> "<span class="id">emit</span>" "<span class="id">emits</span>" <span class="id">actual_emit</span> <span class="id">expected_emit</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_clause_return_component_error">ergo_format_clause_return_component_error</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> "<span class="id">respond</span>" "<span class="id">responds</span>" <span class="id">actual_resp</span> <span class="id">expected_resp</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_format_clause_return_error">ergo_format_clause_return_error</a></span> <span class="id">nsctxt</span> (<span class="id">name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) (<span class="id">actual</span> <span class="id">expected</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">actual_quad</span> := <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#unpack_output_type">unpack_output_type</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual">actual</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">expected_quad</span> := <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#unpack_output_type">unpack_output_type</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected">expected</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">normal_error</span> := <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_clause_return_normal_error">ergo_format_clause_return_normal_error</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual">actual</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected">expected</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">fallback_error</span> := <span class="kwd">fun</span> <span class="id">e</span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_clause_return_fallback_error">ergo_format_clause_return_fallback_error</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual">actual</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected">expected</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2_both">elift2_both</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#normal_error">normal_error</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fallback_error">fallback_error</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual_quad">actual_quad</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected_quad">expected_quad</a></span>.<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_format_function_return_error">ergo_format_function_return_error</a></span> <span class="id">nsctxt</span> (<span class="id">name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) (<span class="id">actual</span> <span class="id">expected</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">actual_s</span> := <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual">actual</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">expected_s</span> := <span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected">expected</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;"<span class="id">Function</span> " ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> ++ " <span class="id">should</span> <span class="kwd">return</span> `" ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expected_s">expected_s</a></span> ++ "' <span class="id">but</span> <span class="id">actually</span> <span class="id">returns</span> `" ++ <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#actual_s">actual_s</a></span> ++ "'".<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="ergo_type_expr">ergo_type_expr</a></span> <span class="id">nsctxt</span> (<span class="id">ctxt</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span>) (<span class="id">expr</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expr">expr</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisContract">EThisContract</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id">prov</span> "<span class="id">No</span> `<span class="id">this</span>' <span class="kwd">in</span> <span class="id">ergoc</span>")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisClause">EThisClause</a></span>   <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id">prov</span> "<span class="id">No</span> `<span class="id">clause</span>' <span class="kwd">in</span> <span class="id">ergoc</span>")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EThisState">EThisState</a></span>    <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id">prov</span> "<span class="id">No</span> `<span class="id">state</span>' <span class="kwd">in</span> <span class="id">ergoc</span>")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EVar">EVar</a></span> <span class="id">prov</span> <span class="id">name</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">opt</span> := <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Assoc.html#lookup">lookup</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">String.string_dec</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context_local_env">type_context_local_env</a></span>)++<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context_global_env">type_context_global_env</a></span>)) <span class="id">name</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#opt">opt</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span> ("<span class="kwd">Variable</span> `" ++ <span class="id">name</span> ++ "' <span class="id">not</span> <span class="id">found</span>.")%<span class="id">string</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EConst">EConst</a></span> <span class="id">prov</span> <span class="id">d</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataTyping.TDataInfer.html#infer_data_type">infer_data_type</a></span> <span class="id">d</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span> "<span class="id">Bad</span> <span class="id">constant</span>.")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ENone">ENone</a></span> <span class="id">prov</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.toption">toption</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbottom">tbottom</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ESome">ESome</a></span> <span class="id">prov</span> <span class="id">e</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.toption">toption</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">e</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EArray">EArray</a></span> <span class="id">prov</span> <span class="id">es</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tcoll">tcoll</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">T</span> <span class="id">new</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">T</span>' =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">new</span>' =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_join">ergoc_type_join</a></span> <span class="id">T</span>' <span class="id">new</span>')<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#new">new</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#T">T</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">es</span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbottom">tbottom</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EUnaryOp">EUnaryOp</a></span> <span class="id">prov</span> <span class="id">op</span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">e</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">t</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_infer_unary_op">ergoc_type_infer_unary_op</a></span> <span class="id">op</span> <span class="id">t</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id">r</span>, <span class="id">_</span>) =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id">r</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_unop_error">ergo_format_unop_error</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id">op</span> <span class="id">t</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">f</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> <span class="id">f</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EBinaryOp">EBinaryOp</a></span> <span class="id">prov</span> <span class="id">op</span> <span class="id">e1</span> <span class="id">e2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">e1</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">t1</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">e2</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">t2</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_infer_binary_op">ergoc_type_infer_binary_op</a></span> <span class="id">op</span> <span class="id">t1</span> <span class="id">t2</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id">r</span>, <span class="id">_</span>, <span class="id">_</span>) =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id">r</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_binop_error">ergo_format_binop_error</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id">op</span> <span class="id">t1</span> <span class="id">t2</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">f</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> <span class="id">f</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">f</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> <span class="id">f</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EIf">EIf</a></span> <span class="id">prov</span> <span class="id">c</span> <span class="id">t</span> <span class="id">f</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">c</span>' =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_subtype_dec">ergoc_type_subtype_dec</a></span> <span class="id">c</span>' <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbool">tbool</a></span> <span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_join">ergoc_type_join</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">t</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">f</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span> "'<span class="id">If</span>' <span class="id">condition</span> <span class="id">not</span> <span class="id">boolean</span>."%<span class="id">string</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">c</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ELet">ELet</a></span> <span class="id">prov</span> <span class="id">n</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> <span class="id">v</span> <span class="id">e</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">vt</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span>' := <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context_update_local_env">type_context_update_local_env</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">n</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#vt">vt</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id">ctxt</span>' <span class="id">e</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">v</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ELet">ELet</a></span> <span class="id">prov</span> <span class="id">n</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">t</span>) <span class="id">v</span> <span class="id">e</span>  =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">fmt_err</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">fun</span> <span class="id">t</span>' <span class="id">vt</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id">prov</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvFunc">ProvFunc</a></span> <span class="id">_</span> <span class="id">fname</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;("<span class="id">Function</span> `" ++ <span class="id">fname</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "' <span class="id">expected</span> <span class="id">argument</span> `"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ <span class="id">n</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "' <span class="id">to</span> <span class="id">be</span> <span class="id">of</span> <span class="id">type</span> `"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id">t</span>')<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "' <span class="id">but</span> <span class="id">was</span> <span class="id">given</span> <span class="id">argument</span> <span class="id">of</span> <span class="id">type</span> `"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#vt">vt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "'." )<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;("<span class="id">The</span> <span class="kwd">let</span> <span class="id">type</span> <span class="id">annotation</span> `"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id">t</span>')<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "' <span class="kwd">for</span> <span class="id">the</span> <span class="id">name</span> `"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ <span class="id">n</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "' <span class="id">does</span> <span class="id">not</span> <span class="kwd">match</span> <span class="id">the</span> <span class="id">actual</span> <span class="id">type</span> `"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#vt">vt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "'.")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">vt</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">t</span>' := (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> <span class="id">t</span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.TypeSystem.RSubtype.html#subtype_dec">subtype_dec</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#vt">vt</a></span> <span class="id">t</span>' <span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span>' :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context_update_local_env">type_context_update_local_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">n</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">t</span>'<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id">ctxt</span>' <span class="id">e</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_err">fmt_err</a></span> <span class="id">t</span>' <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#vt">vt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">v</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ERecord">ERecord</a></span> <span class="id">prov</span> <span class="id">rs</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">sofar</span> <span class="id">next</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift2">eolift2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">sofar</span>' <span class="id">val</span>' =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Program.Basics.html#compose">compose</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_infer_binary_op">ergoc_type_infer_binary_op</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpRecConcat">OpRecConcat</a></span> <span class="id">sofar</span>' <span class="id">val</span>')<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span> "<span class="id">Bad</span> <span class="id">record</span>! <span class="id">Failed</span> <span class="id">to</span> <span class="id">concat</span>."%<span class="id">string</span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#sofar">sofar</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">val</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_infer_unary_op">ergoc_type_infer_unary_op</a></span> (<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpRec">OpRec</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#next">next</a></span>)) <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#val">val</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span> "<span class="id">Bad</span> <span class="id">record</span>! <span class="id">Failed</span> <span class="id">to</span> <span class="id">init</span>."%<span class="id">string</span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#next">next</a></span>))))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">rs</span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#empty_rec_type">empty_rec_type</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ENew">ENew</a></span> <span class="id">prov</span> <span class="id">name</span> <span class="id">rs</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">rs</span>' =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.infer_brand_strict">infer_brand_strict</a></span> (<span class="id">name</span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>) <span class="id">rs</span>')<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_new_error">ergo_format_new_error</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id">name</span> <span class="id">rs</span>'))))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">sofar</span> <span class="id">next</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift2">eolift2</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">sofar</span>' <span class="id">val</span>' =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Program.Basics.html#compose">compose</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_infer_binary_op">ergoc_type_infer_binary_op</a></span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.BinaryOperators.html#OpRecConcat">OpRecConcat</a></span> <span class="id">sofar</span>' <span class="id">val</span>')<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span> "<span class="id">Bad</span> <span class="id">record</span>! <span class="id">Failed</span> <span class="id">to</span> <span class="id">concat</span>."%<span class="id">string</span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#sofar">sofar</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">val</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_infer_unary_op">ergoc_type_infer_unary_op</a></span> (<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Operators.UnaryOperators.html#OpRec">OpRec</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#next">next</a></span>)) <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#val">val</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span> "<span class="id">Bad</span> <span class="id">record</span>! <span class="id">Failed</span> <span class="id">to</span> <span class="id">init</span>."%<span class="id">string</span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#next">next</a></span>))))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">rs</span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#empty_rec_type">empty_rec_type</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFun">ECallFun</a></span> <span class="id">prov</span> <span class="id">fname</span> <span class="id">args</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#function_not_inlined_error">function_not_inlined_error</a></span> <span class="id">prov</span> <span class="id">fname</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#ECallFunInGroup">ECallFunInGroup</a></span> <span class="id">prov</span> <span class="id">gname</span> <span class="id">fname</span> <span class="id">args</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#function_in_group_not_inlined_error">function_in_group_not_inlined_error</a></span> <span class="id">prov</span> <span class="id">gname</span> <span class="id">fname</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EMatch">EMatch</a></span> <span class="id">prov</span> <span class="id">term</span> <span class="id">pes</span> <span class="id">default</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">term</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">f</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> <span class="id">f</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">t0</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">default_result</span> <span class="id">pe</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#pe">pe</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseData">CaseData</a></span> <span class="id">prov</span> <span class="id">d</span>, <span class="id">res</span>) =&gt; <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_infer_data">ergoc_type_infer_data</a></span> <span class="id">d</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span> "<span class="id">Ill</span>-<span class="id">typed</span> <span class="id">data</span> <span class="id">literal</span>!")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">dt</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_join">ergoc_type_join</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#default_result">default_result</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">res</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseWildcard">CaseWildcard</a></span> <span class="id">prov</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>, <span class="id">res</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_join">ergoc_type_join</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#default_result">default_result</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">res</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseLet">CaseLet</a></span> <span class="id">prov</span> <span class="id">name</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>, <span class="id">res</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_join">ergoc_type_join</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#default_result">default_result</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context_update_local_env">type_context_update_local_env</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">name</span> <span class="id">t0</span>) <span class="id">res</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseLetOption">CaseLetOption</a></span> <span class="id">prov</span> <span class="id">name</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>, <span class="id">res</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.unteither">unteither</a></span> <span class="id">t0</span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#default_result">default_result</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id">st</span>, <span class="id">ft</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_join">ergoc_type_join</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#default_result">default_result</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context_update_local_env">type_context_update_local_env</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">name</span> <span class="id">st</span>) <span class="id">res</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseWildcard">CaseWildcard</a></span> <span class="id">prov</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">b</span>), <span class="id">res</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_join">ergoc_type_join</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#default_result">default_result</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">res</span>)<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseLet">CaseLet</a></span> <span class="id">prov</span> <span class="id">name</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">b</span>), <span class="id">res</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_join">ergoc_type_join</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#default_result">default_result</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context_update_local_env">type_context_update_local_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">name</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbrand">tbrand</a></span> (<span class="id">b</span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">res</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id"><a href="ErgoSpec.Common.Utils.Ast.html#CaseLetOption">CaseLetOption</a></span> <span class="id">prov</span> <span class="id">name</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">b</span>), <span class="id">res</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ergoc_type_join">ergoc_type_join</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#default_result">default_result</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context_update_local_env">type_context_update_local_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">name</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbrand">tbrand</a></span> (<span class="id">b</span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">res</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">pes</span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">default</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EForeach">EForeach</a></span> <span class="id">prov</span> ((<span class="id">name</span>,<span class="id">arr</span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>) <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> <span class="id">fn</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">arr</span>' =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">typ</span> =&gt; (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tcoll">tcoll</a></span>) (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context_update_local_env">type_context_update_local_env</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">name</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#typ">typ</a></span>) <span class="id">fn</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_option">eresult_of_option</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.untcoll">untcoll</a></span> <span class="id">arr</span>')<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;("<span class="id">foreach</span> <span class="id">expects</span> <span class="id">an</span> <span class="id">array</span> <span class="id">to</span> <span class="id">iterate</span> <span class="id">over</span>, <span class="id">but</span> <span class="id">was</span> <span class="id">given</span> <span class="id">something</span> <span class="id">of</span> <span class="id">type</span> `" ++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id">arr</span>') ++ "'."))))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span> <span class="id">arr</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Ergo.Lang.Ergo.html#EForeach">EForeach</a></span> <span class="id">prov</span> <span class="id">_</span> <span class="id">_</span> <span class="id">_</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#complex_foreach_in_calculus_error">complex_foreach_in_calculus_error</a></span> <span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergoc_type_function">ergoc_type_function</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">name</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">dctxt</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">func</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_function">ergoc_function</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#func">func</a></span>.(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#functionc_body">functionc_body</a></span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">body</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">tsig</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">map</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#x">x</a></span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#x">x</a></span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#func">func</a></span>.(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#functionc_sig">functionc_sig</a></span>).(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#sigc_params">sigc_params</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">outt</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">eoutt</span> := <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#func">func</a></span>.(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#functionc_sig">functionc_sig</a></span>).(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#sigc_output">sigc_output</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#eoutt">eoutt</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">eoutt</span>' =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">expectedt</span> := <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> <span class="id">eoutt</span>' <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.TypeSystem.RSubtype.html#subtype_dec">subtype_dec</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#outt">outt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expectedt">expectedt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">body_prov</span> := <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#bodyc_annot">bodyc_annot</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#func">func</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#func">func</a></span>.(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#functionc_annot">functionc_annot</a></span>) <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvClause">ProvClause</a></span> <span class="id">_</span> <span class="id">name</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#body_prov">body_prov</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_clause_return_error">ergo_format_clause_return_error</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#outt">outt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expectedt">expectedt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#ProvFunc">ProvFunc</a></span> <span class="id">_</span> <span class="id">name</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#body_prov">body_prov</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_function_return_error">ergo_format_function_return_error</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#outt">outt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expectedt">expectedt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id">_</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#body_prov">body_prov</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_format_function_return_error">ergo_format_function_return_error</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#outt">outt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#expectedt">expectedt</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context_set_local_env">type_context_set_local_env</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#tsig">tsig</a></span>) <span class="id">body</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergoc_type_clause">ergoc_type_clause</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">dctxt</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">cl</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_function">ergoc_function</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> (<span class="id">name</span>,<span class="id">body</span>) := <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#cl">cl</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergoc_type_function">ergoc_type_function</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#name">name</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#body">body</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergoc_type_contract">ergoc_type_contract</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">dctxt</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">coname</span>: <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name">absolute_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">c</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_contract">ergoc_contract</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift_fold_left">elift_fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergoc_type_clause">ergoc_type_clause</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#c">c</a></span>.(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#contractc_clauses">contractc_clauses</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergoc_type_decl">ergoc_type_decl</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">dctxt</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">decl</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_declaration">ergoc_declaration</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> * <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#decl">decl</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#DCExpr">DCExpr</a></span> <span class="id">prov</span> <span class="id">expr</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#x">x</a></span>, <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span>)) (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span> <span class="id">expr</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#DCConstant">DCConstant</a></span> <span class="id">prov</span> <span class="id">name</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> <span class="id">expr</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">expr</span>' := <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span> <span class="id">expr</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">val</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>, <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context_update_global_env">type_context_update_global_env</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span> <span class="id">name</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#val">val</a></span>)) <span class="id">expr</span>'<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#DCConstant">DCConstant</a></span> <span class="id">prov</span> <span class="id">name</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">t</span>) <span class="id">expr</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">fmt_err</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">fun</span> <span class="id">t</span>' <span class="id">vt</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id">prov</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;("<span class="id">The</span> <span class="id">type</span> <span class="id">annotation</span> `"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id">t</span>')<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "' <span class="kwd">for</span> <span class="id">the</span> <span class="id">constant</span> `"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ <span class="id">name</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "' <span class="id">does</span> <span class="id">not</span> <span class="kwd">match</span> <span class="id">its</span> <span class="id">actual</span> <span class="id">type</span> `"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ (<span class="id"><a href="ErgoSpec.Common.Utils.PrintTypedData.html#ergoc_type_to_string">ergoc_type_to_string</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#vt">vt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;++ "'.")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">expr</span>' := <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergo_type_expr">ergo_type_expr</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span> <span class="id">expr</span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">vt</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">t</span>' := (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> <span class="id">t</span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.TypeSystem.RSubtype.html#subtype_dec">subtype_dec</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#vt">vt</a></span> <span class="id">t</span>' <span class="kwd">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span>' :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context_update_global_env">type_context_update_global_env</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span> <span class="id">name</span> <span class="id">t</span>'<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>, <span class="id">ctxt</span>')<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#fmt_err">fmt_err</a></span> <span class="id">t</span>' <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#vt">vt</a></span>)) <span class="id">expr</span>'<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#DCFunc">DCFunc</a></span> <span class="id">prov</span> <span class="id">name</span> <span class="id">func</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">ctxt</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>,<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span>)) (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergoc_type_function">ergoc_type_function</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id">name</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span> <span class="id">func</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#DCContract">DCContract</a></span> <span class="id">prov</span> <span class="id">name</span> <span class="id">contr</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">ctxt</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>,<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ctxt">ctxt</a></span>)) (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergoc_type_contract">ergoc_type_contract</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span> <span class="id">name</span> <span class="id">contr</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergoc_type_module">ergoc_type_module</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nsctxt</span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">dctxt</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">mod</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_module">ergoc_module</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_module">ergoc_module</a></span> * <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#mod">mod</a></span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#x">x</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift_context_fold_left">elift_context_fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ergoc_type_decl">ergoc_type_decl</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#nsctxt">nsctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#mod">mod</a></span>.(<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#modulec_declarations">modulec_declarations</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#dctxt">dctxt</a></span>).<br/>
&nbsp;&nbsp;<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCType.html#ErgoCType">ErgoCType</a></span>.<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
